

LEMMA

If x partially overlaps y and y non-tangentially contains z, then x is not part of z.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp-1 y z)) => (~ (p x z))))))


> revsk
=============================
Step 2

? (((~ (po c1168286 c1168285)) v (~ (ntpp-1 c1168285 c1168284))) v (~ (p c1168286 c1168284)))


> hypdisj
=============================
Step 3

? (~ (p c1168286 c1168284))

1. (ntpp-1 c1168285 c1168284)
2. (po c1168286 c1168285)

> ((~ (p X Z)) <-- (c Y X) (~ (c Y Z)))
|=============================
|Step 4
|
|? (c (f1163233 c1168286 Var49 Var50) c1168286)
|
|1. (p c1168286 c1168284)
|2. (ntpp-1 c1168285 c1168284)
|3. (po c1168286 c1168285)
|
|> ((c (f1163233 Y Z X) Y) <-- (~ (p Y Z)))
|=============================
|Step 5
|
|? (~ (p c1168286 Var49))
|
|1. (~ (c (f1163233 c1168286 Var49 Var50) c1168286))
|2. (p c1168286 c1168284)
|3. (ntpp-1 c1168285 c1168284)
|4. (po c1168286 c1168285)
|
|> ((~ (p X Y)) <-- (po X Y))
|=============================
|Step 6
|
|? (po c1168286 Var49)
|
|1. (p c1168286 Var49)
|2. (~ (c (f1163233 c1168286 Var49 Var50) c1168286))
|3. (p c1168286 c1168284)
|4. (ntpp-1 c1168285 c1168284)
|5. (po c1168286 c1168285)
|
|> hyp
=============================
Step 7

? (~ (c (f1163233 c1168286 c1168285 Var50) c1168284))

1. (p c1168286 c1168284)
2. (ntpp-1 c1168285 c1168284)
3. (po c1168286 c1168285)

> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
|=============================
|Step 8
|
|? (p c1168284 Var56)
|
|1. (c (f1163233 c1168286 c1168285 Var50) c1168284)
|2. (p c1168286 c1168284)
|3. (ntpp-1 c1168285 c1168284)
|4. (po c1168286 c1168285)
|
|> ((p X Y) <-- (pp X Y))
|=============================
|Step 9
|
|? (pp c1168284 Var56)
|
|1. (~ (p c1168284 Var56))
|2. (c (f1163233 c1168286 c1168285 Var50) c1168284)
|3. (p c1168286 c1168284)
|4. (ntpp-1 c1168285 c1168284)
|5. (po c1168286 c1168285)
|
|> ((pp X Y) <-- (ntpp X Y))
|=============================
|Step 10
|
|? (ntpp c1168284 Var56)
|
|1. (~ (pp c1168284 Var56))
|2. (~ (p c1168284 Var56))
|3. (c (f1163233 c1168286 c1168285 Var50) c1168284)
|4. (p c1168286 c1168284)
|5. (ntpp-1 c1168285 c1168284)
|6. (po c1168286 c1168285)
|
|> ((ntpp Y X) <-- (ntpp-1 X Y))
|=============================
|Step 11
|
|? (ntpp-1 Var56 c1168284)
|
|1. (~ (ntpp c1168284 Var56))
|2. (~ (pp c1168284 Var56))
|3. (~ (p c1168284 Var56))
|4. (c (f1163233 c1168286 c1168285 Var50) c1168284)
|5. (p c1168286 c1168284)
|6. (ntpp-1 c1168285 c1168284)
|7. (po c1168286 c1168285)
|
|> hyp
=============================
Step 12

? (~ (c (f1163233 c1168286 c1168285 Var50) c1168285))

1. (c (f1163233 c1168286 c1168285 Var50) c1168284)
2. (p c1168286 c1168284)
3. (ntpp-1 c1168285 c1168284)
4. (po c1168286 c1168285)

> ((~ (c (f1163233 Y Z X) Z)) <-- (~ (p Y Z)))
=============================
Step 13

? (~ (p c1168286 c1168285))

1. (c (f1163233 c1168286 c1168285 Var50) c1168285)
2. (c (f1163233 c1168286 c1168285 Var50) c1168284)
3. (p c1168286 c1168284)
4. (ntpp-1 c1168285 c1168284)
5. (po c1168286 c1168285)

> ((~ (p X Y)) <-- (po X Y))
=============================
Step 14

? (po c1168286 c1168285)

1. (p c1168286 c1168285)
2. (c (f1163233 c1168286 c1168285 Var50) c1168285)
3. (c (f1163233 c1168286 c1168285 Var50) c1168284)
4. (p c1168286 c1168284)
5. (ntpp-1 c1168285 c1168284)
6. (po c1168286 c1168285)

> hyp


LEMMA

Partial overlap implies overlap.
=============================
Step 1

? (all x (all y ((po x y) => (o x y))))


> revsk
=============================
Step 2

? ((~ (po c1173515 c1173514)) v (o c1173515 c1173514))


> hypdisj
=============================
Step 3

? (o c1173515 c1173514)

1. (po c1173515 c1173514)

> ((o X Y) <-- (po X Y))
=============================
Step 4

? (po c1173515 c1173514)

1. (~ (o c1173515 c1173514))
2. (po c1173515 c1173514)

> hyp


LEMMA

Overlap implies connection.
=============================
Step 1

? (all x (all y ((o x y) => (c x y))))


> revsk
=============================
Step 2

? ((~ (o c1178800 c1178799)) v (c c1178800 c1178799))


> hypdisj
=============================
Step 3

? (c c1178800 c1178799)

1. (o c1178800 c1178799)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var48 c1178799)
|
|1. (~ (c c1178800 c1178799))
|2. (o c1178800 c1178799)
|
|> ((p Z X) <-- (~ (c (f1173547 Z X Y) Z)))
|=============================
|Step 5
|
|? (~ (c (f1173547 Var48 c1178799 Var51) Var48))
|
|1. (~ (p Var48 c1178799))
|2. (~ (c c1178800 c1178799))
|3. (o c1178800 c1178799)
|
|> ((~ (c Y X)) <-- (p X Z) (~ (c Y Z)))
||=============================
||Step 6
||
||? (p (f1173564 Var57 Var54) Var54)
||
||1. (c (f1173547 (f1173564 Var57 Var54) c1178799 Var51) (f1173564 Var57 Var54))
||2. (~ (p (f1173564 Var57 Var54) c1178799))
||3. (~ (c c1178800 c1178799))
||4. (o c1178800 c1178799)
||
||> ((p (f1173564 X Y) Y) <-- (o X Y))
||=============================
||Step 7
||
||? (o Var57 Var54)
||
||1. (~ (p (f1173564 Var57 Var54) Var54))
||2. (c (f1173547 (f1173564 Var57 Var54) c1178799 Var51) (f1173564 Var57 Var54))
||3. (~ (p (f1173564 Var57 Var54) c1178799))
||4. (~ (c c1178800 c1178799))
||5. (o c1178800 c1178799)
||
||> hyp
|=============================
|Step 8
|
|? (~ (c (f1173547 (f1173564 c1178800 c1178799) c1178799 Var51) c1178799))
|
|1. (c (f1173547 (f1173564 c1178800 c1178799) c1178799 Var51) (f1173564 c1178800 c1178799))
|2. (~ (p (f1173564 c1178800 c1178799) c1178799))
|3. (~ (c c1178800 c1178799))
|4. (o c1178800 c1178799)
|
|> ((~ (c (f1173547 Y Z X) Z)) <-- (~ (p Y Z)))
|=============================
|Step 9
|
|? (~ (p (f1173564 c1178800 c1178799) c1178799))
|
|1. (c (f1173547 (f1173564 c1178800 c1178799) c1178799 Var51) c1178799)
|2. (c (f1173547 (f1173564 c1178800 c1178799) c1178799 Var51) (f1173564 c1178800 c1178799))
|3. (~ (p (f1173564 c1178800 c1178799) c1178799))
|4. (~ (c c1178800 c1178799))
|5. (o c1178800 c1178799)
|
|> hyp
=============================
Step 10

? (c c1178800 (f1173564 c1178800 c1178799))

1. (~ (c c1178800 c1178799))
2. (o c1178800 c1178799)

> ((c Y X) <-- (c X Y))
=============================
Step 11

? (c (f1173564 c1178800 c1178799) c1178800)

1. (~ (c c1178800 (f1173564 c1178800 c1178799)))
2. (~ (c c1178800 c1178799))
3. (o c1178800 c1178799)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 12
|
|? (p (f1173564 c1178800 Var71) c1178800)
|
|1. (~ (c (f1173564 c1178800 c1178799) c1178800))
|2. (~ (c c1178800 (f1173564 c1178800 c1178799)))
|3. (~ (c c1178800 c1178799))
|4. (o c1178800 c1178799)
|
|> ((p (f1173564 X Y) X) <-- (o X Y))
|=============================
|Step 13
|
|? (o c1178800 Var71)
|
|1. (~ (p (f1173564 c1178800 Var71) c1178800))
|2. (~ (c (f1173564 c1178800 c1178799) c1178800))
|3. (~ (c c1178800 (f1173564 c1178800 c1178799)))
|4. (~ (c c1178800 c1178799))
|5. (o c1178800 c1178799)
|
|> hyp
=============================
Step 14

? (c (f1173564 c1178800 c1178799) (f1173564 c1178800 c1178799))

1. (~ (c (f1173564 c1178800 c1178799) c1178800))
2. (~ (c c1178800 (f1173564 c1178800 c1178799)))
3. (~ (c c1178800 c1178799))
4. (o c1178800 c1178799)

> ((c X X) <--)


LEMMA

Inverse non-tangential proper part implies inverse proper part.
=============================
Step 1

? (all x (all y ((ntpp-1 x y) => (pp-1 x y))))


> revsk
=============================
Step 2

? ((~ (ntpp-1 c1184141 c1184140)) v (pp-1 c1184141 c1184140))


> hypdisj
=============================
Step 3

? (pp-1 c1184141 c1184140)

1. (ntpp-1 c1184141 c1184140)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c1184140 c1184141)

1. (~ (pp-1 c1184141 c1184140))
2. (ntpp-1 c1184141 c1184140)

> ((pp X Y) <-- (ntpp X Y))
=============================
Step 5

? (ntpp c1184140 c1184141)

1. (~ (pp c1184140 c1184141))
2. (~ (pp-1 c1184141 c1184140))
3. (ntpp-1 c1184141 c1184140)

> ((ntpp Y X) <-- (ntpp-1 X Y))
=============================
Step 6

? (ntpp-1 c1184141 c1184140)

1. (~ (ntpp c1184140 c1184141))
2. (~ (pp c1184140 c1184141))
3. (~ (pp-1 c1184141 c1184140))
4. (ntpp-1 c1184141 c1184140)

> hyp


LEMMA

Inverse proper part implies inverse parthood.
=============================
Step 1

? (all x (all y ((pp-1 x y) => (p-1 x y))))


> revsk
=============================
Step 2

? ((~ (pp-1 c1189538 c1189537)) v (p-1 c1189538 c1189537))


> hypdisj
=============================
Step 3

? (p-1 c1189538 c1189537)

1. (pp-1 c1189538 c1189537)

> ((p-1 Y X) <-- (p X Y))
=============================
Step 4

? (p c1189537 c1189538)

1. (~ (p-1 c1189538 c1189537))
2. (pp-1 c1189538 c1189537)

> ((p X Y) <-- (pp X Y))
=============================
Step 5

? (pp c1189537 c1189538)

1. (~ (p c1189537 c1189538))
2. (~ (p-1 c1189538 c1189537))
3. (pp-1 c1189538 c1189537)

> ((pp Y X) <-- (pp-1 X Y))
=============================
Step 6

? (pp-1 c1189538 c1189537)

1. (~ (pp c1189537 c1189538))
2. (~ (p c1189537 c1189538))
3. (~ (p-1 c1189538 c1189537))
4. (pp-1 c1189538 c1189537)

> hyp


LEMMA

Parthood transports connection from part to whole.
=============================
Step 1

? (all x (all y (all z (((p x y) & (c z x)) => (c z y)))))


> revsk
=============================
Step 2

? (((~ (p c1194993 c1194992)) v (~ (c c1194991 c1194993))) v (c c1194991 c1194992))


> hypdisj
=============================
Step 3

? (c c1194991 c1194992)

1. (c c1194991 c1194993)
2. (p c1194993 c1194992)

> ((c Y X) <-- (p Z X) (c Y Z))
|=============================
|Step 4
|
|? (p Var24 c1194992)
|
|1. (~ (c c1194991 c1194992))
|2. (c c1194991 c1194993)
|3. (p c1194993 c1194992)
|
|> hyp
=============================
Step 5

? (c c1194991 c1194993)

1. (~ (c c1194991 c1194992))
2. (c c1194991 c1194993)
3. (p c1194993 c1194992)

> hyp


LEMMA

Split x,z into disconnection or connection.
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp-1 y z)) => ((dc x z) v (c x z))))))


> revsk
=============================
Step 2

? (((~ (po c1200604 c1200603)) v (~ (ntpp-1 c1200603 c1200602))) v ((dc c1200604 c1200602) v (c c1200604 c1200602)))


> hypdisj
=============================
Step 3

? (c c1200604 c1200602)

1. (~ (dc c1200604 c1200602))
2. (ntpp-1 c1200603 c1200602)
3. (po c1200604 c1200603)

> ((c X Y) <-- (~ (dc X Y)))
=============================
Step 4

? (~ (dc c1200604 c1200602))

1. (~ (c c1200604 c1200602))
2. (~ (dc c1200604 c1200602))
3. (ntpp-1 c1200603 c1200602)
4. (po c1200604 c1200603)

> hyp


LEMMA

In the connected case, x,z are ec or po or z is part of x.
=============================
Step 1

? (all x (all y (all z ((((po x y) & (ntpp-1 y z)) & (c x z)) => (((ec x z) v (po x z)) v (p z x))))))


> revsk
=============================
Step 2

? ((((~ (po c1206481 c1206480)) v (~ (ntpp-1 c1206480 c1206479))) v (~ (c c1206481 c1206479))) v (((ec c1206481 c1206479) v (po c1206481 c1206479)) v (p c1206479 c1206481)))


> hypdisj
=============================
Step 3

? (p c1206479 c1206481)

1. (~ (po c1206481 c1206479))
2. (~ (ec c1206481 c1206479))
3. (c c1206481 c1206479)
4. (ntpp-1 c1206480 c1206479)
5. (po c1206481 c1206480)

> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||=============================
||Step 4
||
||? (o c1206481 c1206479)
||
||1. (~ (p c1206479 c1206481))
||2. (~ (po c1206481 c1206479))
||3. (~ (ec c1206481 c1206479))
||4. (c c1206481 c1206479)
||5. (ntpp-1 c1206480 c1206479)
||6. (po c1206481 c1206480)
||
||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||=============================
|||Step 5
|||
|||? (c c1206481 c1206479)
|||
|||1. (~ (o c1206481 c1206479))
|||2. (~ (p c1206479 c1206481))
|||3. (~ (po c1206481 c1206479))
|||4. (~ (ec c1206481 c1206479))
|||5. (c c1206481 c1206479)
|||6. (ntpp-1 c1206480 c1206479)
|||7. (po c1206481 c1206480)
|||
|||> hyp
||=============================
||Step 6
||
||? (~ (ec c1206481 c1206479))
||
||1. (~ (o c1206481 c1206479))
||2. (~ (p c1206479 c1206481))
||3. (~ (po c1206481 c1206479))
||4. (~ (ec c1206481 c1206479))
||5. (c c1206481 c1206479)
||6. (ntpp-1 c1206480 c1206479)
||7. (po c1206481 c1206480)
||
||> hyp
|=============================
|Step 7
|
|? (~ (p c1206481 c1206479))
|
|1. (~ (p c1206479 c1206481))
|2. (~ (po c1206481 c1206479))
|3. (~ (ec c1206481 c1206479))
|4. (c c1206481 c1206479)
|5. (ntpp-1 c1206480 c1206479)
|6. (po c1206481 c1206480)
|
|> ((~ (p X Z)) <-- (po X Y) (ntpp-1 Y Z))
||=============================
||Step 8
||
||? (po c1206481 Var37)
||
||1. (p c1206481 c1206479)
||2. (~ (p c1206479 c1206481))
||3. (~ (po c1206481 c1206479))
||4. (~ (ec c1206481 c1206479))
||5. (c c1206481 c1206479)
||6. (ntpp-1 c1206480 c1206479)
||7. (po c1206481 c1206480)
||
||> hyp
|=============================
|Step 9
|
|? (ntpp-1 c1206480 c1206479)
|
|1. (p c1206481 c1206479)
|2. (~ (p c1206479 c1206481))
|3. (~ (po c1206481 c1206479))
|4. (~ (ec c1206481 c1206479))
|5. (c c1206481 c1206479)
|6. (ntpp-1 c1206480 c1206479)
|7. (po c1206481 c1206480)
|
|> hyp
=============================
Step 10

? (~ (po c1206481 c1206479))

1. (~ (p c1206479 c1206481))
2. (~ (po c1206481 c1206479))
3. (~ (ec c1206481 c1206479))
4. (c c1206481 c1206479)
5. (ntpp-1 c1206480 c1206479)
6. (po c1206481 c1206480)

> hyp


LEMMA

Converse parthood plus failure of forward parthood gives inverse proper part.
=============================
Step 1

? (all x (all y (((p y x) & (~ (p x y))) => (pp-1 x y))))


> revsk
=============================
Step 2

? (((~ (p c1212967 c1212968)) v (p c1212968 c1212967)) v (pp-1 c1212968 c1212967))


> hypdisj
=============================
Step 3

? (pp-1 c1212968 c1212967)

1. (~ (p c1212968 c1212967))
2. (p c1212967 c1212968)

> ((pp-1 Y X) <-- (pp X Y))
=============================
Step 4

? (pp c1212967 c1212968)

1. (~ (pp-1 c1212968 c1212967))
2. (~ (p c1212968 c1212967))
3. (p c1212967 c1212968)

> ((pp Y X) <-- (p Y X) (~ (p X Y)))
|=============================
|Step 5
|
|? (p c1212967 c1212968)
|
|1. (~ (pp c1212967 c1212968))
|2. (~ (pp-1 c1212968 c1212967))
|3. (~ (p c1212968 c1212967))
|4. (p c1212967 c1212968)
|
|> hyp
=============================
Step 6

? (~ (p c1212968 c1212967))

1. (~ (pp c1212967 c1212968))
2. (~ (pp-1 c1212968 c1212967))
3. (~ (p c1212968 c1212967))
4. (p c1212967 c1212968)

> hyp


LEMMA

Inverse proper part splits into tangential or non-tangential inverse proper part.
=============================
Step 1

? (all x (all y ((pp-1 x y) => ((tpp-1 x y) v (ntpp-1 x y)))))


> revsk
=============================
Step 2

? ((~ (pp-1 c1219606 c1219605)) v ((tpp-1 c1219606 c1219605) v (ntpp-1 c1219606 c1219605)))


> hypdisj
=============================
Step 3

? (ntpp-1 c1219606 c1219605)

1. (~ (tpp-1 c1219606 c1219605))
2. (pp-1 c1219606 c1219605)

> ((ntpp-1 Y X) <-- (ntpp X Y))
=============================
Step 4

? (ntpp c1219605 c1219606)

1. (~ (ntpp-1 c1219606 c1219605))
2. (~ (tpp-1 c1219606 c1219605))
3. (pp-1 c1219606 c1219605)

> ((ntpp Z X) <-- (pp Z X) (~ (ec (f1213083 Z X Y) Z)))
|=============================
|Step 5
|
|? (pp c1219605 c1219606)
|
|1. (~ (ntpp c1219605 c1219606))
|2. (~ (ntpp-1 c1219606 c1219605))
|3. (~ (tpp-1 c1219606 c1219605))
|4. (pp-1 c1219606 c1219605)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 6
|
|? (pp-1 c1219606 c1219605)
|
|1. (~ (pp c1219605 c1219606))
|2. (~ (ntpp c1219605 c1219606))
|3. (~ (ntpp-1 c1219606 c1219605))
|4. (~ (tpp-1 c1219606 c1219605))
|5. (pp-1 c1219606 c1219605)
|
|> hyp
=============================
Step 7

? (~ (ec (f1213083 c1219605 c1219606 Var44) c1219605))

1. (~ (ntpp c1219605 c1219606))
2. (~ (ntpp-1 c1219606 c1219605))
3. (~ (tpp-1 c1219606 c1219605))
4. (pp-1 c1219606 c1219605)

> ((~ (ec X Y)) <-- (pp Y Z) (ec X Z) (~ (tpp Y Z)))
||=============================
||Step 8
||
||? (pp c1219605 Var50)
||
||1. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
||2. (~ (ntpp c1219605 c1219606))
||3. (~ (ntpp-1 c1219606 c1219605))
||4. (~ (tpp-1 c1219606 c1219605))
||5. (pp-1 c1219606 c1219605)
||
||> ((pp Y X) <-- (pp-1 X Y))
||=============================
||Step 9
||
||? (pp-1 Var50 c1219605)
||
||1. (~ (pp c1219605 Var50))
||2. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
||3. (~ (ntpp c1219605 c1219606))
||4. (~ (ntpp-1 c1219606 c1219605))
||5. (~ (tpp-1 c1219606 c1219605))
||6. (pp-1 c1219606 c1219605)
||
||> hyp
|=============================
|Step 10
|
|? (ec (f1213083 c1219605 c1219606 Var44) c1219606)
|
|1. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
|2. (~ (ntpp c1219605 c1219606))
|3. (~ (ntpp-1 c1219606 c1219605))
|4. (~ (tpp-1 c1219606 c1219605))
|5. (pp-1 c1219606 c1219605)
|
|> ((ec (f1213083 Y Z X) Z) <-- (~ (ntpp Y Z)) (pp Y Z))
||=============================
||Step 11
||
||? (~ (ntpp c1219605 c1219606))
||
||1. (~ (ec (f1213083 c1219605 c1219606 Var44) c1219606))
||2. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
||3. (~ (ntpp c1219605 c1219606))
||4. (~ (ntpp-1 c1219606 c1219605))
||5. (~ (tpp-1 c1219606 c1219605))
||6. (pp-1 c1219606 c1219605)
||
||> hyp
|=============================
|Step 12
|
|? (pp c1219605 c1219606)
|
|1. (~ (ec (f1213083 c1219605 c1219606 Var44) c1219606))
|2. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
|3. (~ (ntpp c1219605 c1219606))
|4. (~ (ntpp-1 c1219606 c1219605))
|5. (~ (tpp-1 c1219606 c1219605))
|6. (pp-1 c1219606 c1219605)
|
|> ((pp Y X) <-- (pp-1 X Y))
|=============================
|Step 13
|
|? (pp-1 c1219606 c1219605)
|
|1. (~ (pp c1219605 c1219606))
|2. (~ (ec (f1213083 c1219605 c1219606 Var44) c1219606))
|3. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
|4. (~ (ntpp c1219605 c1219606))
|5. (~ (ntpp-1 c1219606 c1219605))
|6. (~ (tpp-1 c1219606 c1219605))
|7. (pp-1 c1219606 c1219605)
|
|> hyp
=============================
Step 14

? (~ (tpp c1219605 c1219606))

1. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
2. (~ (ntpp c1219605 c1219606))
3. (~ (ntpp-1 c1219606 c1219605))
4. (~ (tpp-1 c1219606 c1219605))
5. (pp-1 c1219606 c1219605)

> ((~ (tpp Y X)) <-- (~ (tpp-1 X Y)))
=============================
Step 15

? (~ (tpp-1 c1219606 c1219605))

1. (tpp c1219605 c1219606)
2. (ec (f1213083 c1219605 c1219606 Var44) c1219605)
3. (~ (ntpp c1219605 c1219606))
4. (~ (ntpp-1 c1219606 c1219605))
5. (~ (tpp-1 c1219606 c1219605))
6. (pp-1 c1219606 c1219605)

> hyp


LEMMA

Split into dc(x,z) or c(x,z). In the connected case use Lemma8. If p(z,x), combine with Lemma1 to get pp-1(x,z), then Lemma10 gives tpp-1(x,z) or ntpp-1(x,z).
=============================
Step 1

? (all x (all y (all z (((po x y) & (ntpp-1 y z)) => (((((dc x z) v (ec x z)) v (po x z)) v (tpp-1 x z)) v (ntpp-1 x z))))))


> revsk
=============================
Step 2

? (((~ (po c1226397 c1226396)) v (~ (ntpp-1 c1226396 c1226395))) v (((((dc c1226397 c1226395) v (ec c1226397 c1226395)) v (po c1226397 c1226395)) v (tpp-1 c1226397 c1226395)) v (ntpp-1 c1226397 c1226395)))


> hypdisj
=============================
Step 3

? (ntpp-1 c1226397 c1226395)

1. (~ (tpp-1 c1226397 c1226395))
2. (~ (po c1226397 c1226395))
3. (~ (ec c1226397 c1226395))
4. (~ (dc c1226397 c1226395))
5. (ntpp-1 c1226396 c1226395)
6. (po c1226397 c1226396)

> ((ntpp-1 X Y) <-- (pp-1 X Y) (~ (tpp-1 X Y)))
|=============================
|Step 4
|
|? (pp-1 c1226397 c1226395)
|
|1. (~ (ntpp-1 c1226397 c1226395))
|2. (~ (tpp-1 c1226397 c1226395))
|3. (~ (po c1226397 c1226395))
|4. (~ (ec c1226397 c1226395))
|5. (~ (dc c1226397 c1226395))
|6. (ntpp-1 c1226396 c1226395)
|7. (po c1226397 c1226396)
|
|> ((pp-1 X Y) <-- (p Y X) (~ (p X Y)))
||=============================
||Step 5
||
||? (p c1226395 c1226397)
||
||1. (~ (pp-1 c1226397 c1226395))
||2. (~ (ntpp-1 c1226397 c1226395))
||3. (~ (tpp-1 c1226397 c1226395))
||4. (~ (po c1226397 c1226395))
||5. (~ (ec c1226397 c1226395))
||6. (~ (dc c1226397 c1226395))
||7. (ntpp-1 c1226396 c1226395)
||8. (po c1226397 c1226396)
||
||> ((p Y X) <-- (o X Y) (~ (p X Y)) (~ (po X Y)))
||||=============================
||||Step 6
||||
||||? (o c1226397 c1226395)
||||
||||1. (~ (p c1226395 c1226397))
||||2. (~ (pp-1 c1226397 c1226395))
||||3. (~ (ntpp-1 c1226397 c1226395))
||||4. (~ (tpp-1 c1226397 c1226395))
||||5. (~ (po c1226397 c1226395))
||||6. (~ (ec c1226397 c1226395))
||||7. (~ (dc c1226397 c1226395))
||||8. (ntpp-1 c1226396 c1226395)
||||9. (po c1226397 c1226396)
||||
||||> ((o X Y) <-- (c X Y) (~ (ec X Y)))
|||||=============================
|||||Step 7
|||||
|||||? (c c1226397 c1226395)
|||||
|||||1. (~ (o c1226397 c1226395))
|||||2. (~ (p c1226395 c1226397))
|||||3. (~ (pp-1 c1226397 c1226395))
|||||4. (~ (ntpp-1 c1226397 c1226395))
|||||5. (~ (tpp-1 c1226397 c1226395))
|||||6. (~ (po c1226397 c1226395))
|||||7. (~ (ec c1226397 c1226395))
|||||8. (~ (dc c1226397 c1226395))
|||||9. (ntpp-1 c1226396 c1226395)
|||||10. (po c1226397 c1226396)
|||||
|||||> ((c X Y) <-- (~ (dc X Y)))
|||||=============================
|||||Step 8
|||||
|||||? (~ (dc c1226397 c1226395))
|||||
|||||1. (~ (c c1226397 c1226395))
|||||2. (~ (o c1226397 c1226395))
|||||3. (~ (p c1226395 c1226397))
|||||4. (~ (pp-1 c1226397 c1226395))
|||||5. (~ (ntpp-1 c1226397 c1226395))
|||||6. (~ (tpp-1 c1226397 c1226395))
|||||7. (~ (po c1226397 c1226395))
|||||8. (~ (ec c1226397 c1226395))
|||||9. (~ (dc c1226397 c1226395))
|||||10. (ntpp-1 c1226396 c1226395)
|||||11. (po c1226397 c1226396)
|||||
|||||> hyp
||||=============================
||||Step 9
||||
||||? (~ (ec c1226397 c1226395))
||||
||||1. (~ (o c1226397 c1226395))
||||2. (~ (p c1226395 c1226397))
||||3. (~ (pp-1 c1226397 c1226395))
||||4. (~ (ntpp-1 c1226397 c1226395))
||||5. (~ (tpp-1 c1226397 c1226395))
||||6. (~ (po c1226397 c1226395))
||||7. (~ (ec c1226397 c1226395))
||||8. (~ (dc c1226397 c1226395))
||||9. (ntpp-1 c1226396 c1226395)
||||10. (po c1226397 c1226396)
||||
||||> hyp
|||=============================
|||Step 10
|||
|||? (~ (p c1226397 c1226395))
|||
|||1. (~ (p c1226395 c1226397))
|||2. (~ (pp-1 c1226397 c1226395))
|||3. (~ (ntpp-1 c1226397 c1226395))
|||4. (~ (tpp-1 c1226397 c1226395))
|||5. (~ (po c1226397 c1226395))
|||6. (~ (ec c1226397 c1226395))
|||7. (~ (dc c1226397 c1226395))
|||8. (ntpp-1 c1226396 c1226395)
|||9. (po c1226397 c1226396)
|||
|||> ((~ (p X Z)) <-- (po X Y) (ntpp-1 Y Z))
||||=============================
||||Step 11
||||
||||? (po c1226397 Var55)
||||
||||1. (p c1226397 c1226395)
||||2. (~ (p c1226395 c1226397))
||||3. (~ (pp-1 c1226397 c1226395))
||||4. (~ (ntpp-1 c1226397 c1226395))
||||5. (~ (tpp-1 c1226397 c1226395))
||||6. (~ (po c1226397 c1226395))
||||7. (~ (ec c1226397 c1226395))
||||8. (~ (dc c1226397 c1226395))
||||9. (ntpp-1 c1226396 c1226395)
||||10. (po c1226397 c1226396)
||||
||||> hyp
|||=============================
|||Step 12
|||
|||? (ntpp-1 c1226396 c1226395)
|||
|||1. (p c1226397 c1226395)
|||2. (~ (p c1226395 c1226397))
|||3. (~ (pp-1 c1226397 c1226395))
|||4. (~ (ntpp-1 c1226397 c1226395))
|||5. (~ (tpp-1 c1226397 c1226395))
|||6. (~ (po c1226397 c1226395))
|||7. (~ (ec c1226397 c1226395))
|||8. (~ (dc c1226397 c1226395))
|||9. (ntpp-1 c1226396 c1226395)
|||10. (po c1226397 c1226396)
|||
|||> hyp
||=============================
||Step 13
||
||? (~ (po c1226397 c1226395))
||
||1. (~ (p c1226395 c1226397))
||2. (~ (pp-1 c1226397 c1226395))
||3. (~ (ntpp-1 c1226397 c1226395))
||4. (~ (tpp-1 c1226397 c1226395))
||5. (~ (po c1226397 c1226395))
||6. (~ (ec c1226397 c1226395))
||7. (~ (dc c1226397 c1226395))
||8. (ntpp-1 c1226396 c1226395)
||9. (po c1226397 c1226396)
||
||> hyp
|=============================
|Step 14
|
|? (~ (p c1226397 c1226395))
|
|1. (~ (pp-1 c1226397 c1226395))
|2. (~ (ntpp-1 c1226397 c1226395))
|3. (~ (tpp-1 c1226397 c1226395))
|4. (~ (po c1226397 c1226395))
|5. (~ (ec c1226397 c1226395))
|6. (~ (dc c1226397 c1226395))
|7. (ntpp-1 c1226396 c1226395)
|8. (po c1226397 c1226396)
|
|> ((~ (p X Z)) <-- (po X Y) (ntpp-1 Y Z))
||=============================
||Step 15
||
||? (po c1226397 Var61)
||
||1. (p c1226397 c1226395)
||2. (~ (pp-1 c1226397 c1226395))
||3. (~ (ntpp-1 c1226397 c1226395))
||4. (~ (tpp-1 c1226397 c1226395))
||5. (~ (po c1226397 c1226395))
||6. (~ (ec c1226397 c1226395))
||7. (~ (dc c1226397 c1226395))
||8. (ntpp-1 c1226396 c1226395)
||9. (po c1226397 c1226396)
||
||> hyp
|=============================
|Step 16
|
|? (ntpp-1 c1226396 c1226395)
|
|1. (p c1226397 c1226395)
|2. (~ (pp-1 c1226397 c1226395))
|3. (~ (ntpp-1 c1226397 c1226395))
|4. (~ (tpp-1 c1226397 c1226395))
|5. (~ (po c1226397 c1226395))
|6. (~ (ec c1226397 c1226395))
|7. (~ (dc c1226397 c1226395))
|8. (ntpp-1 c1226396 c1226395)
|9. (po c1226397 c1226396)
|
|> hyp
=============================
Step 17

? (~ (tpp-1 c1226397 c1226395))

1. (~ (ntpp-1 c1226397 c1226395))
2. (~ (tpp-1 c1226397 c1226395))
3. (~ (po c1226397 c1226395))
4. (~ (ec c1226397 c1226395))
5. (~ (dc c1226397 c1226395))
6. (ntpp-1 c1226396 c1226395)
7. (po c1226397 c1226396)

> hyp
